package org.act.BPEL2Automata.automata;

import java.util.LinkedList;

import org.act.BPEL2Automata.automata.module.ComplexLogicalFormulaImp;
import org.act.BPEL2Automata.automata.module.LabelFunction;
import org.act.BPEL2Automata.automata.module.LogicalFormula;
import org.act.BPEL2Automata.automata.module.Message;
import org.act.BPEL2Automata.automata.module.SimpleLogicalFormulaImp;
import org.act.BPEL2Automata.automata.module.State;
import org.act.BPEL2Automata.automata.module.StatePair;
import org.act.BPEL2Automata.automata.module.TransitionFunction;
import org.act.BPEL2Automata.automata.module.TransitionMatrix;

/**
 * 
 * <b>AutomataImp</b> provides one static method to calculate 
 * bi-simulation equivalence of two automatas(actFSA).
 * @author baoxiwu<bb@feijiao.info>,ACT,Beihang University
 * @version 0.9.0
 * @since 2010-03-24
 * 
 */
public class AutomataImp {
	//COMMON MESSAGE SET SHARED BY ALL THE AUTOMATAIMP INSTANCES.
	private static final LinkedList<Message> commonMessageSet = new LinkedList<Message>();
	
	public static LinkedList<StatePair> bisimulationResult = new LinkedList<StatePair>();
	
	
	//7-tuples : <Q,Sigma,delta,s,F,L>
	private LinkedList<State> stateSet = new LinkedList<State>();
	private LinkedList<Message> messageSet = AutomataImp.commonMessageSet;
	private TransitionFunction tf = new TransitionFunction();
	private State startState = new State();
	private LinkedList<State> finalStateSet = new LinkedList<State>();
	private LabelFunction labelFunction = new LabelFunction();
	
	
	public AutomataImp(){
	//empty
	}
	
	
	public AutomataImp(LinkedList<State> stateSet,LinkedList<Message> messageSet,TransitionFunction tf,State startState,LinkedList<State> finalStateSet,LabelFunction labelFunction){
		this.stateSet = stateSet;
		this.messageSet = messageSet;
		this.tf = tf;
		this.startState = startState;
		this.finalStateSet = finalStateSet;
		this.labelFunction = labelFunction;
	}
	
	
	public static void clearCache(){
		AutomataImp.bisimulationResult = new LinkedList<StatePair>();
	}
	
	//setter and getter methods.
	public void setStateSet(LinkedList<State> stateSet){
		this.stateSet = stateSet;
	}
	
	public void setStateSet(State state){
		this.stateSet.add(state);
	}
	
	public LinkedList<State> getStateSet(){
		return this.stateSet;
	}
	
	public void setMessageSet(LinkedList<Message> messageSet){
		this.messageSet.addAll(messageSet);
	}
	
	public void setMessageSet(Message message){
		this.messageSet.add(message);
	}
	
	public LinkedList<Message> getMessageSet(){
		return this.messageSet;
	}
	
	public void setTransitionFunction(TransitionFunction tf){
		this.tf = tf;
	}
	
	public TransitionFunction getTransitionFunction(){
		return this.tf;
	}
	
	public void setStartState(State startState){
		this.startState = startState;
	}
	
	public State getStartState(){
		return this.startState;
	}
	
	public void setFinalStateSet(LinkedList<State> finalStateSet){
		this.finalStateSet = finalStateSet;
	}
	
	public void setFinalStateSet(State finalState){
		this.finalStateSet.add(finalState);
	}
	
	public LinkedList<State> getFinalStateSet(){
		return this.finalStateSet;
	}
	
	public void setLabelFunction(LabelFunction labelFunction){
		this.labelFunction = labelFunction;
	}
	
	public LabelFunction getLabelFunction(){
		return this.labelFunction;
	}
	
	/**
	 * This static method converts one SubAutomataImp object 
	 * to one AutomataImp object.
	 * @param one SubAutomataImp object to be converted.
	 * @return AutomataImp object that converted from one SubAutomataImp object 
	 */
	public static AutomataImp toAutomataImp(SubAutomataImp automata){
		LinkedList<State> newFinalStateSet = new  LinkedList<State>();
		
		//CORE operations
		//merge automata's F and T.
		newFinalStateSet.addAll(automata.getFinalStateSet());
		newFinalStateSet.addAll(automata.getTerminationStateSet());
		
		AutomataImp tmp = new AutomataImp(automata.getStateSet(),automata.getMessageSet(),automata.getTransitionFunction(),automata.getStartState(),newFinalStateSet,automata.getLabelFunction());
		
		return tmp;
	}
	
	
	//TODO TESTING WANTED.
	/**
	 * This static method uesd to judge whether two automatons 
	 * are bisimulation equivalent.
	 * return bisimulation relation set if bisimilar,
	 * otherwise, the states causing non-bisimulation.
	 */
	public static boolean calBisimulation(AutomataImp automataA,AutomataImp automataB){
		LinkedList<StatePair> R = new LinkedList<StatePair>();
		StatePair sp = new StatePair(automataA.getStartState(),automataB.getStartState());
		R.add(sp);
		
		int q_cur = 0,q_end = 0;
		boolean bsFlag = true;
		State q1 = null,q2 = null;
		TransitionMatrix tm = new TransitionMatrix();
		
		
		while(q_cur <= q_end){
			q1 = R.get(q_cur).getStateX();
			q2 = R.get(q_cur).getStateY();
			
			
			//the states should be both final states or both non-final states if they are bisimilar
			if(!((automataA.getFinalStateSet().contains(q1) && automataB.getFinalStateSet().contains(q2)) ||
					(!(automataA.getFinalStateSet().contains(q1)) && !(automataB.getFinalStateSet().contains(q2))))){
				//marked as a spot state pair
				R.get(q_cur).setIsBisimilar(false);
				
				bsFlag = false;
				
				q_cur++;
				
				continue;
			}
			
			
			for(int i = 0; i < automataA.getMessageSet().size(); i++){
				State q11 = automataA.getTransitionFunction().getByStartStateAndMessage(q1, automataA.getMessageSet().get(i));
				State q22 = automataB.getTransitionFunction().getByStartStateAndMessage(q2, automataA.getMessageSet().get(i));
				
				if(q11 != null && q22!= null){
					LogicalFormula lfa = automataA.getLabelFunction().getByKey(q1);
					LogicalFormula lfb = automataB.getLabelFunction().getByKey(q2);
					
					if(lfa instanceof SimpleLogicalFormulaImp){
						SimpleLogicalFormulaImp slf = (SimpleLogicalFormulaImp)lfa;
						
						if(slf.getMessage() == automataA.getMessageSet().get(i)){
							slf.setValue(true);
						}
					}
					else{
						ComplexLogicalFormulaImp clf = (ComplexLogicalFormulaImp)lfa;
						
						LinkedList<SimpleLogicalFormulaImp> SLFList = clf.getSLFbyStartState(q1);
						
						for(int j = 0; j < SLFList.size(); j++){
							if(SLFList.get(j).getMessage() == automataA.getMessageSet().get(i)){
								SLFList.get(j).setValue(true);
							}
							if(SLFList.get(j).getLogicalFormulaType() == SimpleLogicalFormulaImp.NON_VALID_OR_INVALID_LOGICAL_FORMULA && 
									SLFList.get(j).getMessage() == null){
								SLFList.get(j).setValue(true);
							}
						}
					}
					
					
					if(lfb instanceof SimpleLogicalFormulaImp){
						SimpleLogicalFormulaImp slf = (SimpleLogicalFormulaImp)lfb;
						
						if(slf.getMessage() == automataB.getMessageSet().get(i)){
							slf.setValue(true);
						}
					}
					else{
						ComplexLogicalFormulaImp clf = (ComplexLogicalFormulaImp)lfb;
						
						LinkedList<SimpleLogicalFormulaImp> SLFList = clf.getSLFbyStartState(q2);
						
						for(int j = 0; j < SLFList.size(); j++){
							if(SLFList.get(j).getMessage() == automataB.getMessageSet().get(i)){
								SLFList.get(j).setValue(true);
							}
							if(SLFList.get(j).getLogicalFormulaType() == SimpleLogicalFormulaImp.NON_VALID_OR_INVALID_LOGICAL_FORMULA && 
									SLFList.get(j).getMessage() == null){
								SLFList.get(j).setValue(true);
							}
						}
					}
					
					
					//TODO SPECIAL FOCUS WANTED.
					tm.add(q_cur, i, new StatePair(q11,q22));
				}
			}
			
			
			
			//TODO invoke the parent's calculate method or the children's ?
			//System.out.println("calculate : " + automataA.getLabelFunction().getByKey(q1).calculate());
			//System.out.println("calculate : " + automataB.getLabelFunction().getByKey(q2).calculate());
			
			
			if(automataA.getLabelFunction().getByKey(q1).calculate() &&
					automataB.getLabelFunction().getByKey(q2).calculate()){
				for(int i = 0; i < automataA.getMessageSet().size(); i++){
					if(tm.get(q_cur, i) != null &&
							!(R.contains(tm.get(q_cur, i)))){
						q_end++;
						R.add(tm.get(q_cur, i));
					}
				}
			}
			else{
				R.getLast().setIsBisimilar(false);
				bsFlag = false;
			}
			
			q_cur++;
		}
		
		if(bsFlag == true){
			bisimulationResult.addAll(R);
			return true;
		}
		else{
			LinkedList<StatePair> spot = new LinkedList<StatePair>();
			
			for(int i = 0; i < R.size(); i++){
				if(R.get(i).getIsBisimilar() == false){
					spot.add(R.get(i));
				}
			}
			
			bisimulationResult.addAll(spot);
			return false;
		}
	}
	
	//check status of subFSA object.
	//IT'S NOT NECESSARY TO KEEP AS A PRODUCT.
	//REMOVE THIS METHOD.
	public String toString(){
		String result = "";
		
		//result += "Name : " + this.getClass().getFields() + "\n";
		
		result += "State Set : \n";
		for(int i = 0; i < this.getStateSet().size(); i++){
			result += ("\ts" + this.getStateSet().get(i).getID() + "\n"); 
		}
		
		result += "Message Set : \n";
		for(int i = 0; i < this.getMessageSet().size(); i++){
			result += ("\tmes" + this.getMessageSet().get(i).getID());
			result += ("\n\t\tmt = " + this.getMessageSet().get(i).getMessageType().getName() + 
					"\n\t\tpl = " + this.getMessageSet().get(i).getPartnerLink().getName() +
					"\n\t\tpt = " + this.getMessageSet().get(i).getPortType().getName() + 
					"\n\t\top = " + this.getMessageSet().get(i).getOperation().getName() +
					"\n\t\tdir = " + this.getMessageSet().get(i).getDirection() + "\n");
		}
		
		result += "TransitionFunction : \n";
		//System.err.println(this.getTransitionFunction().getTransitionRuleList().size());
		for(int i = 0; i < this.getTransitionFunction().getTransitionRuleList().size(); i++){
			
			String tmp = this.getTransitionFunction().getTransitionRuleList().get(i).getEndState().getID();
			
			result += ("\ts" +this.getTransitionFunction().getTransitionRuleList().get(i).getStartState().getID() + "_mes" + this.getTransitionFunction().getTransitionRuleList().get(i).getMessage().getID() + "->s" + tmp + "\n"); 
		}
		
		result += ("Start State : \n\ts" + this.getStartState().getID()) + "\n";
		
		result += "\tstart-asSourceList : \n";
		for(int i = 0; i < this.getStartState().getSourceList().size(); i++){
			result += ("\t\t" + this.getStartState().getSourceList().get(i) + "\n");
		}
		
		result += "\tstart-asTargetList : \n";
		for(int i = 0; i < this.getStartState().getTargetList().size(); i++){
			result += ("\t\t" + this.getStartState().getTargetList().get(i) + "\n");
		}
		
		
		result += "Final State Set : \n";
		for(int i = 0; i < this.getFinalStateSet().size(); i++){
			result += ("\ts" + this.getFinalStateSet().get(i).getID() + "\n"); 
			
			result += "\tfinal-asSourceList : \n";
			for(int j = 0; j < this.getFinalStateSet().get(i).getSourceList().size(); j++){
				result += ("\t\t" + this.getFinalStateSet().get(i).getSourceList().get(j) + "\n");
			}
			
			result += "\tfinal-asTargetList : \n";
			for(int j = 0; j < this.getFinalStateSet().get(i).getTargetList().size(); j++){
				result += ("\t\t" + this.getFinalStateSet().get(i).getTargetList().get(j) + "\n");
			}
		}
		
		
		result += "Label Function : \n";
		
		for(int i = 0; i < this.getLabelFunction().getLogicalFormulaList().size(); i++){
			if(this.getLabelFunction().getLogicalFormulaList().get(i) instanceof SimpleLogicalFormulaImp){
				result += ((SimpleLogicalFormulaImp)this.getLabelFunction().getLogicalFormulaList().get(i)).toString();
			}
			else{
				result += ((ComplexLogicalFormulaImp)this.getLabelFunction().getLogicalFormulaList().get(i)).toString();
			}
		}
		
		return result;
	}
}
